Skip to content

fix(rt): resolve thunk(operandCopy) in projection traversal#956

Draft
Stevengre wants to merge 7 commits intomasterfrom
jh/fix-thunk-projection
Draft

fix(rt): resolve thunk(operandCopy) in projection traversal#956
Stevengre wants to merge 7 commits intomasterfrom
jh/fix-thunk-projection

Conversation

@Stevengre
Copy link
Contributor

@Stevengre Stevengre commented Feb 28, 2026

Summary

  • Add thunk-aware projection traversal rules for read/move-read/write/borrow continuations over thunk(operandCopy(place(...))).
  • Add #isThunkOperandCopy guard so terminal projection rules do not match too early on unresolved thunked copy-place values.
  • Add/refresh prove-rs integration cases covering these thunk-projection paths.

Context

Projection traversal could get stuck when a projected value is thunk(operandCopy(place(...))), especially in iterator/closure borrow paths.

Red vs Green

RED (stuck frontier):

#traverseProjection(toLocal(I), thunk(operandCopy(place(local(I), PLACEPROJ))), PROJS, CTXTS)
  ~> #forRef(MUT, META)

No complete continuation for this thunked projection/borrow shape.

GREEN (new explicit continuation):

#traverseProjection(... thunk(operandCopy(place(local(I), PLACEPROJ))), PROJS, CTXTS) ~> #forRef(...)
=> #mkRef(toLocal(I), appendP(#projectionsFor(CTXTS), appendP(PLACEPROJ, PROJS)), MUT, #lookupMaybeTy(#typeForRef(...)), META)

and terminal .ProjectionElems read rules are guarded by notBool #isThunkOperandCopy(VAL).

…w creation

When a value is thunked as thunk(operandCopy(place(...))), projection
traversal and borrow creation had no rules to resolve the thunk, causing
stuck #traverseProjection ~> #readProjection / #forRef terms.

Add #isThunkOperandCopy predicate and four #traverseProjection rules
that compose remaining projections onto the thunked place and delegate
to existing operand evaluation:
- Copy-read: resolve to operandCopy with composed place
- Move-read: emit #writeMoved then resolve the copy
- Write: delegate to #setLocalValue on composed place
- Borrow (#forRef): materialize #mkRef directly to avoid re-traversal

Guard existing .ProjectionElems terminal rules with
notBool #isThunkOperandCopy(VAL) to prevent premature matching.

Tests: iter-copied-take-next-thunk-fail.rs,
       iter-map-eq-copied-take-thunk-fail.rs
Stevengre and others added 6 commits February 28, 2026 14:24
Add a rule for `aggregateKindClosure` to construct closures as
`Aggregate(variantIdx(0), ARGS)`, matching the existing tuple and ADT
aggregate handling.

Add an `[owise]` fallback to `#setTupleArgs` for `Value` arguments
that are not wrapped in an `Aggregate` tuple. This handles closure-call
paths where a single argument is passed directly.

Test: `closure-no-capture.rs` — a non-capturing closure passed through
a generic `FnOnce` call. Exercises the `#setTupleArgs` fallback for
unwrapped single-value arguments.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant